CVC5: Build interpolant sequence in reverse for better performance - #704

Nice observation, but this might only holds for our use case in CPAchecker (and the tested analysis; IMC). There are 2 questions that we need to ask:

• users can choose to do this themselves. Do we want to deviate from the default just because it is better in some instances? Furthermore, we don't want to impose this without communicating it. And if we do that (and we should), we can also in general add a note that users should test whether switching the interpolation groups is useful for them. That way we provide independent advice without imposing any behavior.
• wouldn't it be better if we just cache the interpolation prover until the stack is changed and use our default implementation for sequential (and tree) interpolants? This would allow us to get more interpolants out of CVC5 in general, and more efficiently as well.

wouldn't it be better if we just cache the interpolation prover until the stack is changed

Hmm, I'm not sure what you mean by "caching" here. My idea was that it would be more efficient to reuse the same solver to calculate all interpolants of the sequence, rather than opening a new one for each of them. Unfortunately this is somewhat difficult with the API that CVC5 provides for interpolation:

public Term getInterpolant(Term conj)

Get an interpolant. Given that A->B is valid, this function determines a term I over the shared variables
of A and B, such that A->I and I->B are valid. A is the current set of assertions and B is the
conjecture, given as conj.

So, to interpolate we need to push A onto a new solver stack, and then call getInterpolant with B as its argument. When calculating an interpolation sequence, this is rather awkward in the forward direction as we get a completely different A for each interpolation step:

A -> B -> C -> D -> false

I = itp(    A, B -> C -> D -> false)
J = itp(I & B, C -> D -> false)
K = itp(J & C, D -> false)

The implementation for itp looks something like this with CVC5:

Term itp(A, B) {
  solver.push()
  solver.assertFormula(A)
  var r = solver.getInterpolant(B)
  solver.pop()
  return r
}

So, while we can reuse the same solver, we have to clear the entire stack for each step, which means there won't be much of an advantage left over just opening a new solver instance

Reversing the order of the interpolants helps with this as we can then keep the As on the solver stack:

K = itp(A & B & C, D -> false)
J = itp(A & B    , C -> K)
I = itp(A        , B -> J)

This means we can start by pushing A, B and C on the solver stack, and then for each new interpolant we only need to clear the last assertion, while keeping the rest. My idea was, that this may help the solver as it allows it to keep some of the state while calculating the interpolation steps of the sequence

In practice the difference seems to be rather small, and you're right, that most of the speed up was from just reversing the order. Here are some benchmarks:

The runs were (from top to bottom):

• main
• reversed interpolation groups
• reusing the solver
• this branch

This branch still seems to have some edge over just reversing the groups:

However, it's much less than I was expecting

Nice observation, but this might only holds for our use case in CPAchecker (and the tested analysis; IMC)

Do we have any other benchmarks for interpolation? I've done some optimization for Yices2 aswell, however, it's hard to know what to aim for without a good benchmark

Nevermind my last comment. My idea does not work with CVC5s API.

Do we have any other benchmarks for interpolation? I've done some optimization for Yices2 aswell, however, it's hard to know what to aim for without a good benchmark

Predicate Abstraction and IMC are our only relevant tools to benchmark interpolation.